What

Phase 2 of the Layer-10 echo-residue work (phase 1 = #34). Makes the
reversal residue a first-class linear value. The checker's residue
stack now carries Linear<Echo<T>> (was a bare Echo<T>): push_echo_residue
wraps the residue in Type::Linear, so the consumed-once discipline is
explicit in the carried type, and the single linear use is discharged by
the matching take_echo_residue pop in a later reverse.

The only non-comment code change is that one-line wrap; the rest is the
Idris proof, tests, spec, and docs.

The design decision (worth a look)

A reversal log is an affine capability consumed linearly:

• Linear consumption — when you do reverse, you consume one specific
  residue exactly once (reverseLinear's (1 e : Echo f y)). Replaying the
  same log twice is rejected: the residue has already been popped, so the
  second reverse is ReverseWithoutResidue.
• Affine retention — a reversible block need not be paired with a
  reverse. An undo capability that is never exercised is dropped at the
  body boundary, not flagged. Reversibility is a capability, usually unused.

The opposite — strict "must-reverse" linearity, where an un-reversed residue
is a LinearNotConsumed error — is deliberately rejected: it conflates
having an inverse with applying it, and is poor agent ergonomics. Three
new tests lock the affine drop in so a future change cannot silently tighten
it.

Formal model

proofs/idris2/EchoResidueLinear.idr (%default total, zero believe_me,
idris2 --check clean):

• reverseLinear consumes (1 e : Echo f y) — Idris2's quantity 1 is
  the "consumed exactly once" proof, mirroring 007's planned Linear<Echo<T>>;
• reverseLinearCorrect — recovered input maps back to y (intrinsic);
• ResidueCell (Holding/Spent) — the residue carried as agent state
  between handler invocations;
• takeForReverse — a later handler consumes the cell linearly (Spent → Nothing);
• holdingReverses / spentDoesNotReverse — cross-handler reversal succeeds
  iff a residue was retained;
• cellMode — bridges a cell back to the phase-1 Reversibility mode.

Verified locally

• idris2 --check EchoResidueLinear.idr → exit 0 (and dependency EchoResidue.idr)
• cargo test -p oo7-core → 883 lib tests pass (incl. 3 new L10 phase-2 tests), 0 fail
• cargo fmt -- --check → 0 diffs
• cargo clippy -- -D warnings (CI-equivalent, no --all-targets) → exit 0
• A2ML validator on .machine_readable/6a2/ → 0 errors

Still open (its own rung)

Cross-handler named residues need residue-binding surface syntax
(let undo = reversible {…} … later reverse undo). The formal model
(ResidueCell) is already in place; only the grammar change is missing, and
because the grammar is Harvard-guarded that is kept as a separate, carefully-
scoped rung. Until then cross-handler reversal is conservatively rejected by
per-body isolation (sound, if incomplete).

Docs updated in lockstep

spec/TYPE-SYSTEM-SPEC.adoc §11b.4, spec/OPERATIONAL-SEMANTICS.adoc §11.4
(planned → landed), CHANGELOG.md, docs/echo-residue-integration.adoc
(phase-2 section + design-decision subsection + still-open rung), and 6a2
STATE.a2ml.

Note: repo CI may still be gated by the GitHub Actions billing/spending-limit
rejection documented in the session log (account-owner action). All gates
above were therefore verified locally.

https://claude.ai/code/session_018CaSgNjNURC7ocsyjYh9We

Generated by Claude Code